package com.starview.star.compiler.transform;

import java.util.ArrayList;
import java.util.Collection;
import java.util.HashMap;
import java.util.List;
import java.util.Map;
import java.util.Map.Entry;
import java.util.SortedMap;
import java.util.Stack;
import java.util.TreeMap;

import com.starview.platform.data.IValue;
import com.starview.platform.data.type.ContractConstraint;
import com.starview.platform.data.type.FieldConstraint;
import com.starview.platform.data.type.FieldTypeConstraint;
import com.starview.platform.data.type.Freshen;
import com.starview.platform.data.type.IType;
import com.starview.platform.data.type.ITypeConstraint;
import com.starview.platform.data.type.Location;
import com.starview.platform.data.type.Refresher;
import com.starview.platform.data.type.Subsume;
import com.starview.platform.data.type.Type;
import com.starview.platform.data.type.TypeConstraintException;
import com.starview.platform.data.type.TypeExp;
import com.starview.platform.data.type.TypeUtils;
import com.starview.platform.data.type.TypeVar;
import com.starview.platform.data.type.UniversalType;
import com.starview.star.compiler.CompilerUtils;
import com.starview.star.compiler.ErrorReport;
import com.starview.star.compiler.FreeVariables;
import com.starview.star.compiler.ast.Abstract;
import com.starview.star.compiler.ast.Apply;
import com.starview.star.compiler.ast.IAbstract;
import com.starview.star.compiler.ast.Name;
import com.starview.star.compiler.canonical.FieldAccess;
import com.starview.star.compiler.canonical.FunctionLiteral;
import com.starview.star.compiler.canonical.IContentAction;
import com.starview.star.compiler.canonical.IContentExpression;
import com.starview.star.compiler.canonical.IContentPattern;
import com.starview.star.compiler.canonical.IStatement;
import com.starview.star.compiler.canonical.LetAction;
import com.starview.star.compiler.canonical.LetTerm;
import com.starview.star.compiler.canonical.MemoExp;
import com.starview.star.compiler.canonical.MethodVariable;
import com.starview.star.compiler.canonical.Overloaded;
import com.starview.star.compiler.canonical.OverloadedFieldAccess;
import com.starview.star.compiler.canonical.OverloadedVariable;
import com.starview.star.compiler.canonical.PatternAbstraction;
import com.starview.star.compiler.canonical.RecordTerm;
import com.starview.star.compiler.canonical.Resolved;
import com.starview.star.compiler.canonical.Sequence;
import com.starview.star.compiler.canonical.VarDeclaration;
import com.starview.star.compiler.canonical.VarEntry;
import com.starview.star.compiler.canonical.Variable;
import com.starview.star.compiler.standard.StandardNames;
import com.starview.star.compiler.type.ContractDependencies;
import com.starview.star.compiler.type.DictInfo;
import com.starview.star.compiler.type.Dictionary;
import com.starview.star.compiler.type.TypeContracts;
import com.starview.star.compiler.type.Visibility;
import com.starview.star.compiler.util.AccessMode;
import com.starview.star.compiler.util.Pair;

/**
 * Implement aspects of the function overloading from the SR compiler
 * 
 * @author fgm
 * 
 */
public class OverLoader extends Substitution
{
  ErrorReport errors;
  private int varNo = 0;
  private Stack<Pair<IType, IContentExpression>> dict = new Stack<Pair<IType, IContentExpression>>();
  private Dictionary localCxt;

  public OverLoader(Dictionary cxt, Dictionary localCxt, ErrorReport errors)
  {
    super(cxt);
    this.localCxt = localCxt;
    this.errors = errors;

    install(new FunctionLiteralTransform());
    install(new MethodVariableTransform());
    install(new VariableOverload());
    install(new OverloadedOverload());
    install(new OverloadedVariableOverload());
    install(new OverloadFieldAccess());
    install(new PatternAbstractionTransform());
    install(new OverloadResolved());
    install(new VarEntryTrans());
    install(new LetTermTrans());
    install(new LetActionTrans());
    install(new RecordTransform());
    install(new ActionSequenceTransform());
    install(new VarDeclarationTransform());
  }

  public static void declarePrimitiveImplementation(String contract, String method, IType rawType, String escape)
  {
    PrimitiveOverloader.declarePrimitiveImplementation(contract, method, rawType, escape);
  }

  private class FunctionLiteralTransform implements TransformExpression
  {
    @Override
    public Class<? extends IContentExpression> transformClass()
    {
      return FunctionLiteral.class;
    }

    @Override
    public IContentExpression transformExp(IContentExpression exp)
    {
      FunctionLiteral fun = (FunctionLiteral) exp;
      int mark = dict.size();
      try {
        IType funType = fun.getType();
        if (TypeUtils.isOverloadedType(funType)) {
          IContentPattern args[] = fun.getArgs();
          for (IContentPattern arg : args) {
            if (arg instanceof Variable)
              dict.push(Pair.pair(arg.getType(), (IContentExpression) arg));
          }
        }

        IContentPattern trArgs[] = transformPatterns(fun.getArgs());
        IContentExpression trRes = transform(fun.getBody());

        Variable[] freeVars = FreeVariables.freeFreeVars(trArgs, trRes, localCxt);

        String funName = fun.getName();
        IContentExpression newName = substitute(funName);
        if (newName != null) {
          funName = ((Variable) newName).getName();
          funType = newName.getType();
        }

        return new FunctionLiteral(exp.getLoc(), funName, funType, trArgs, trRes, freeVars);
      } finally {
        dict.setSize(mark);
      }
    }
  }

  private class PatternAbstractionTransform implements TransformExpression
  {
    @Override
    public Class<? extends IContentExpression> transformClass()
    {
      return PatternAbstraction.class;
    }

    @Override
    public IContentExpression transformExp(IContentExpression exp)
    {
      PatternAbstraction ptn = (PatternAbstraction) exp;

      int mark = dict.size();
      try {
        if (TypeUtils.isOverloadedType(ptn.getType())) {
          IContentPattern args[] = ptn.getArgs();
          for (IContentPattern arg : args) {
            if (arg instanceof Variable)
              dict.push(Pair.pair(arg.getType(), (IContentExpression) arg));
          }
        }

        String ptnName = ptn.getName();
        IContentExpression newName = substitute(ptnName);
        if (newName != null)
          ptnName = ((Variable) newName).getName();

        IContentPattern trMatch = transform(ptn.getMatch());
        IContentExpression trRes = transform(ptn.getResult());

        Variable[] freeVars = FreeVariables.freeFreeVars(new IContentPattern[] { trMatch }, trRes, localCxt);

        return new PatternAbstraction(exp.getLoc(), ptnName, exp.getType(), trMatch, trRes, freeVars);
      } finally {
        dict.setSize(mark);
      }
    }
  }

  private IContentExpression locateDictVar(IType type)
  {
    // Need to process the stack in top-down order
    for (int ix = dict.size(); ix > 0; ix--) {
      Pair<IType, IContentExpression> entry = dict.get(ix - 1);
      if (entry.left().equals(type))
        return entry.right();
    }

    return null;
  }

  private class VarEntryTrans implements TransformStatement
  {
    @Override
    public Class<? extends IStatement> transformClass()
    {
      return VarEntry.class;
    }

    @Override
    public IStatement transformStmt(IStatement stmt)
    {
      VarEntry vEntry = (VarEntry) stmt;
      final IContentExpression transformedValue = transform(vEntry.getValue());

      return new VarEntry(vEntry.getDefined(), vEntry.getLoc(), transform(vEntry.getVarPattern()), transformedValue,
          vEntry.isReadOnly(), vEntry.getVisibility());
    }
  }

  private class VarDeclarationTransform implements TransformAction
  {
    @Override
    public IContentAction transformAction(IContentAction act)
    {
      VarDeclaration decl = (VarDeclaration) act;

      return new VarDeclaration(act.getLoc(), transform(decl.getPattern()), decl.isReadOnly(), transform(decl
          .getValue()));
    }

    @Override
    public Class<? extends IContentAction> transformClass()
    {
      return VarDeclaration.class;
    }
  }

  private class MethodVariableTransform implements TransformExpression
  {
    @Override
    public Class<? extends IContentExpression> transformClass()
    {
      return MethodVariable.class;
    }

    @Override
    public IContentExpression transformExp(IContentExpression var)
    {
      MethodVariable method = (MethodVariable) var;

      TypeExp contract = (TypeExp) method.getContract();
      Location loc = var.getLoc();
      IType varType = method.getType();

      // First look for primitive implementations
      String name = method.getName();
      String escape = PrimitiveOverloader.getPrimitive((TypeExp) method.getContract(), name);
      if (escape != null)
        return new Variable(method.getLoc(), method.getType(), escape);

      IContentExpression cVar = resolve(loc, contract);
      if (cVar == null)
        cVar = locateDictVar(contract);
      if (cVar != null && !TypeUtils.isTypeVar(cVar.getType()))
        return FieldAccess.create(loc, varType, cVar, name);
      else
        return method;// May end up being converted at another level
    }
  }

  private class OverloadedOverload implements TransformExpression
  {
    @Override
    public Class<? extends IContentExpression> transformClass()
    {
      return Overloaded.class;
    }

    @Override
    public IContentExpression transformExp(IContentExpression exp)
    {
      Overloaded var = (Overloaded) exp;
      IContentExpression inner = transform(var.getInner());

      Location loc = var.getLoc();

      IType overType = var.getDictType();

      IType reqs[] = TypeUtils.getOverloadRequirements(overType);
      IContentExpression args[] = new IContentExpression[reqs.length];

      for (int ix = 0; ix < args.length; ix++) {
        IType reqType = reqs[ix];

        assert reqType instanceof TypeExp;

        args[ix] = resolve(var.getLoc(), reqType);

        if (args[ix] == null)
          return var; // not ready to overload, signal for overloading later
      }

      if (inner instanceof Variable)
        inner = ((Variable) inner).underLoad(); // convert an overloaded variable to a regular one.

      return new Resolved(loc, TypeUtils.getOverloadedType(overType), overType, inner, args);
    }
  }

  private class OverloadFieldAccess implements TransformExpression
  {
    @Override
    public Class<? extends IContentExpression> transformClass()
    {
      return OverloadedFieldAccess.class;
    }

    @Override
    public IContentExpression transformExp(IContentExpression exp)
    {
      OverloadedFieldAccess var = (OverloadedFieldAccess) exp;
      IContentExpression overRoute = transform(var.getRecord());

      Location loc = var.getLoc();

      IType overType = var.getDictType();

      IType reqs[] = TypeUtils.getOverloadRequirements(overType);
      IContentExpression args[] = new IContentExpression[reqs.length];

      for (int ix = 0; ix < args.length; ix++) {
        IType reqType = reqs[ix];

        assert reqType instanceof TypeExp;

        args[ix] = resolve(var.getLoc(), reqType);

        if (args[ix] == null)
          return var; // not ready to overload, signal for overloading later
      }

      return new Resolved(loc, TypeUtils.getOverloadedType(overType), overType, new FieldAccess(loc, overType,
          overRoute, var.getField()), args);
    }
  }

  private class OverloadResolved implements TransformExpression
  {

    @Override
    public IContentExpression transformExp(IContentExpression exp)
    {
      return reresolve((Resolved) exp);
    }

    private IContentExpression reresolve(Resolved res)
    {
      IContentExpression over = res.getOver();
      IType dictType = res.getDictType();
      Location loc = res.getLoc();

      IType[] reqTypes = TypeUtils.getOverloadRequirements(dictType);
      if (over instanceof Variable && TypeContracts.isContractFallbackName(((Variable) over).getName())) {
        assert reqTypes.length == 0;
        IContentExpression resolved = resolve(loc, res.getType());

        if (resolved != null && resolved != res)
          return resolved;
        else
          return res;
      } else {
        IContentExpression args[] = res.getDicts();
        IContentExpression nArgs[] = null;
        argLoop: for (int ix = 0; ix < args.length; ix++) {
          IContentExpression arg = args[ix];
          if (arg instanceof Resolved)
            arg = reresolve((Resolved) arg);
          else if (arg == null) // special case for initial resolved case
            arg = resolve(loc, reqTypes[ix]);

          if (arg != args[ix]) {
            if (nArgs == null) {
              nArgs = new IContentExpression[args.length];
              for (int jx = 0; jx < ix; jx++)
                nArgs[jx] = args[jx];
            }
            nArgs[ix] = arg;
            continue argLoop;
          }

          if (nArgs != null)
            nArgs[ix] = arg;
        }

        if (nArgs != null)
          return new Resolved(loc, TypeUtils.getOverloadedType(dictType), dictType, over, nArgs);
        else
          return res;
      }
    }

    @Override
    public Class<? extends IContentExpression> transformClass()
    {
      return Resolved.class;
    }
  }

  private class VariableOverload extends VariableTransform
  {
    @Override
    public Class<? extends IContentExpression> transformClass()
    {
      return Variable.class;
    }

    /**
     * Transforms a variable reference to a function call -- if the referenced value is a reference
     * to an overloaded variable
     */
    @Override
    public IContentExpression transformExp(IContentExpression exp)
    {
      Variable var = (Variable) exp;

      IType varType = var.getType();
      String varName = var.getName();

      IContentExpression subst = substitute(varName);
      if (subst != null && isConsistent(varType, subst.getType(), exp.getLoc())) {
        if (subst instanceof OverloadedVariable)
          return resolveOverloaded((OverloadedVariable) subst);
        else
          return subst;
      } else
        return exp;
    }
  }

  private boolean isConsistent(IType lhsType, IType rhsType, Location loc)
  {
    return Subsume.test(lhsType, rhsType, loc, localCxt);
  }

  private class OverloadedVariableOverload extends VariableTransform
  {
    @Override
    public Class<? extends IContentExpression> transformClass()
    {
      return OverloadedVariable.class;
    }

    /**
     * Transforms an overloaded variable reference to a function call -- if we can resolve it
     * properly
     */
    @Override
    public IContentExpression transformExp(IContentExpression exp)
    {
      OverloadedVariable var = (OverloadedVariable) exp;

      IContentExpression subst = substitute(var.getName());
      if (subst != null && isConsistent(subst.getType(), var.getType(), var.getLoc())) {
        if (subst instanceof OverloadedVariable)
          var = (OverloadedVariable) subst;
        else
          return subst;
      }

      return resolveOverloaded(var);
    }
  }

  private class LetTermTrans implements TransformExpression
  {
    @Override
    public Class<? extends IContentExpression> transformClass()
    {
      return LetTerm.class;
    }

    @Override
    public IContentExpression transformExp(IContentExpression exp)
    {
      LetTerm let = (LetTerm) exp;
      Dictionary current = localCxt;

      localCxt = localCxt.fork();

      for (IStatement stmt : let.getEnvironment()) {
        if (stmt instanceof VarEntry) {
          VarEntry vEntry = (VarEntry) stmt;
          if (vEntry.getVarPattern() instanceof Variable) {
            Variable var = vEntry.getVariable();
            localCxt.declareVar(var.getName(), var, vEntry.isReadOnly(), vEntry.getVisibility(), true);
          }
        }
      }

      List<IStatement> newEnv = new ArrayList<IStatement>();
      for (IStatement entry : let.getEnvironment()) {
        newEnv.add(transform(entry));
      }

      LetTerm transformedBound = new LetTerm(exp.getLoc(), transform(let.getBoundExp()), newEnv);

      localCxt = current;
      return transformedBound;
    }
  }

  private class LetActionTrans implements TransformAction
  {
    @Override
    public Class<? extends IContentAction> transformClass()
    {
      return LetAction.class;
    }

    @Override
    public IContentAction transformAction(IContentAction exp)
    {
      LetAction let = (LetAction) exp;
      Dictionary current = localCxt;

      localCxt = localCxt.fork();

      for (IStatement stmt : let.getEnvironment()) {
        if (stmt instanceof VarEntry) {
          VarEntry vEntry = (VarEntry) stmt;
          if (vEntry.getVarPattern() instanceof Variable) {
            Variable var = vEntry.getVariable();
            localCxt.declareVar(var.getName(), var, vEntry.isReadOnly(), vEntry.getVisibility(), true);
          }
        }
      }

      List<IStatement> newEnv = new ArrayList<IStatement>();
      for (IStatement entry : let.getEnvironment()) {
        newEnv.add(transform(entry));
      }

      LetAction transformedBound = new LetAction(exp.getLoc(), newEnv, transform(let.getBoundAction()));

      localCxt = current;
      return transformedBound;
    }
  }

  private class RecordTransform implements TransformExpression
  {

    @Override
    public Class<? extends IContentExpression> transformClass()
    {
      return RecordTerm.class;
    }

    @Override
    public IContentExpression transformExp(IContentExpression exp)
    {
      RecordTerm record = (RecordTerm) exp;
      Dictionary current = localCxt;

      localCxt = localCxt.fork();
      SortedMap<String, IContentExpression> nEls = new TreeMap<String, IContentExpression>();

      IContentExpression fun = transform(record.getFun());

      for (Entry<String, IContentExpression> entry : record.getArguments().entrySet()) {
        nEls.put(entry.getKey(), transform(entry.getValue()));
      }

      localCxt = current;

      return new RecordTerm(exp.getLoc(), exp.getType(), fun, nEls);
    }
  }

  private class ActionSequenceTransform implements TransformAction
  {
    @Override
    public IContentAction transformAction(IContentAction act)
    {
      Sequence seq = (Sequence) act;
      List<IContentAction> lst = new ArrayList<IContentAction>();
      for (IContentAction acts : seq.getActions())
        lst.add(transform(acts));
      return new Sequence(act.getLoc(), act.getType(), lst);
    }

    @Override
    public Class<? extends IContentAction> transformClass()
    {
      return Sequence.class;
    }
  }

  private IContentExpression resolve(Location loc, IType type)
  {
    type = TypeUtils.deRef(type);

    IContentExpression dictVar = locateDictVar(type);
    if (dictVar != null)
      return dictVar;
    else if ((type instanceof TypeExp || type instanceof Type)) {
      String instanceName = instanceFunName(type);
      if (localCxt.isDefinedVar(instanceName))
        return checkInstance(loc, type, instanceName);
      else if (TypeUtils.isGroundSurface(type) || (TypeUtils.isVarSurface(type) && !varsInScope(type))) {
        instanceName = TypeContracts.contractFallbackName(type);
        if (localCxt.isDefinedVar(instanceName))
          return checkInstance(loc, type, instanceName);
      }
    }
    return null;
  }

  private boolean varsInScope(IType tp)
  {
    for (IType arg : TypeUtils.typeArgs(tp)) {
      arg = TypeUtils.deRef(arg);
      if (arg instanceof TypeVar) {
        if (localCxt.typeExists(((TypeVar) arg).getVarName()))
          return true;
      }
    }
    return false;
  }

  private IContentExpression checkInstance(Location loc, IType type, String instanceName)
  {
    DictInfo instance = localCxt.varReference(instanceName);
    // If the instance is not null but has a variable type, then it is a
    // marker
    // declaration; not the final one. So we do not resolve for it yet.
    if (instance != null && !TypeUtils.isTypeVar(instance.getType())) {
      IType instanceType = instance.getType();
      IType instType = TypeUtils.isOverloadedType(instanceType) ? TypeUtils.refreshOverloaded(instanceType) : Freshen
          .freshenForUse(instanceType);

      if (TypeUtils.isOverloadedType(instType)) {
        IType instArgs[] = TypeUtils.getOverloadRequirements(instType);
        IType conBoundType = TypeUtils.getOverloadedType(instType);

        try {
          Subsume.subsume(type, conBoundType, loc, localCxt);
        } catch (TypeConstraintException e) {
          errors.reportError("cannot resolve: " + type + "\nbecause " + e.getMessage(), Location
              .merge(loc, e.getLocs()));
          return null;
        }

        IContentExpression args[] = new IContentExpression[instArgs.length];
        for (int ix = 0; ix < args.length; ix++) {
          assert TypeUtils.deRef(instArgs[ix]) instanceof TypeExp;
          TypeExp argType = (TypeExp) instArgs[ix];
          IContentExpression cVar = resolve(loc, argType);

          if (cVar == null)
            cVar = locateDictVar(argType);
          if (cVar == null)
            return null;

          args[ix] = cVar;
        }

        IContentExpression over = instance.getVariable();
        if (over instanceof OverloadedVariable)
          over = new Variable(over.getLoc(), instType, ((OverloadedVariable) over).getName());
        return new Resolved(loc, type, instType, over, args);
      } else
        return instance.getVariable();
    }
    return null;
  }

  public static VarEntry instanceFunction(Location loc, String funName, IType implType,
      IContentExpression implementation, Dictionary cxt, ErrorReport errors, Visibility visibility)
  {
    IType genImplType = Refresher.generalize(implType, cxt);
    IType dictType = computeDictionaryType(genImplType, loc, AccessMode.readOnly);

    Dictionary instDict = cxt.fork();
    OverLoader over = new OverLoader(instDict, cxt, errors);

    int varNo = 0;

    IType[] reqTypes = TypeUtils.getOverloadRequirements(dictType);
    Variable reqVars[] = new Variable[reqTypes.length];

    for (int ix = 0; ix < reqTypes.length; ix++) {
      IType reqType = reqTypes[ix];

      Variable dictVar = reqVars[ix] = new Variable(loc, reqType, reqType.typeLabel() + varNo++);
      instDict.declareVar(dictVar.getName(), dictVar, AccessMode.readOnly, Visibility.priVate, true);
      over.dict.push(Pair.pair(reqType, (IContentExpression) dictVar));
    }

    implementation = over.transform(implementation);

    if (reqTypes.length > 0) {
      Variable[] iFree = FreeVariables.freeFreeVars(reqVars, implementation, instDict);

      implementation = new FunctionLiteral(loc, funName, dictType, reqVars, implementation, iFree);
      return new VarEntry(loc, new Variable(loc, dictType, funName), implementation, AccessMode.readOnly, visibility);
    } else {

      Variable[] freeVars = FreeVariables.findFreeVars(implementation, cxt);
      implementation = new MemoExp(loc, implementation, freeVars);
      return new VarEntry(loc, new Variable(loc, dictType, funName), implementation, AccessMode.readOnly, visibility);
    }
  }

  public static String instanceFunName(IType type)
  {
    StringBuilder bldr = new StringBuilder();
    String sep = "";
    for (IType arg : TypeUtils.typeArgs(type)) {
      arg = TypeUtils.deRef(arg);
      if (!TypeUtils.isDetermines(arg)) {
        bldr.append(sep);
        IType arg1 = arg;
        arg1 = TypeUtils.deRef(arg1);
        if (TypeUtils.isTypeVar(arg1) && !((TypeVar) arg1).isReadOnly())
          bldr.append("_");
        else
          bldr.append(arg1.typeLabel());
        sep = "_";
      }
    }
    return instanceFunName(type.typeLabel(), bldr.toString());
  }

  public static String originalInstanceFunName(IType type)
  {
    StringBuilder bldr = new StringBuilder();
    String sep = "";
    for (IType arg : TypeUtils.typeArgs(type)) {
      arg = TypeUtils.deRef(arg);
      if (!TypeUtils.isDetermines(arg)) {
        bldr.append(sep);

        if (TypeUtils.isTypeVar(arg))
          bldr.append(((TypeVar) arg).getOriginalName());
        else
          bldr.append(arg.typeLabel());
        sep = "_";
      }
    }
    return instanceFunName(type.typeLabel(), bldr.toString());
  }

  public static String instanceFunName(String abTypeName, String typeLabel)
  {
    return abTypeName + "#" + typeLabel;
  }

  public static String instanceFunName(IAbstract tp)
  {
    tp = CompilerUtils.unwrapQuants(tp);

    if (Abstract.isBinary(tp, StandardNames.WHERE))
      return instanceFunName(Abstract.binaryLhs(tp));
    else if (Abstract.isParenTerm(tp))
      return instanceFunName(Abstract.deParen(tp));
    else {
      StringBuilder bldr = new StringBuilder();

      if (Abstract.isBinary(tp, StandardNames.OVER) || Abstract.isBinary(tp, StandardNames.OF)) {
        IAbstract con = Abstract.deParen(Abstract.binaryLhs(tp));
        IAbstract args = Abstract.binaryRhs(tp);

        if (con instanceof Name)
          bldr.append(TypeContracts.contractImplTypeName(Abstract.getId(con)));
        bldr.append("#");

        if (Abstract.isTupleTerm(args) && !Abstract.isParenTerm(args)) {
          String sep = "";
          for (IValue a : ((Apply) args).getArgs()) {
            bldr.append(sep);
            sep = "_";
            instFunArgName((IAbstract) a, bldr);
          }
        } else
          instFunArgName(args, bldr);
      }

      return bldr.toString();
    }
  }

  private static void instFunArgName(IAbstract arg, StringBuilder bldr)
  {
    arg = Abstract.deParen(arg);
    if (Abstract.isBinary(arg, StandardNames.WHERE))
      instFunArgName(Abstract.binaryLhs(arg), bldr);
    else if (Abstract.isIdentifier(arg))
      bldr.append(Abstract.getId(arg));
    else if (Abstract.isBinary(arg, StandardNames.OF) && Abstract.isIdentifier(Abstract.binaryLhs(arg)))
      bldr.append(Abstract.getId(Abstract.binaryLhs(arg)));
    else if (Abstract.isTupleTerm(arg))
      bldr.append(TypeUtils.tupleLabel(Abstract.tupleArity(arg)));
    else if (CompilerUtils.isAnonAggConLiteral(arg))
      bldr.append(CompilerUtils.anonRecordTypeLabel(arg));
    else
      bldr.append("_");
  }

  public static VarEntry overload(ErrorReport errors, VarEntry defn, Dictionary cxt)
  {
    OverLoader overloader = new OverLoader(cxt, cxt, errors);
    return overloader.overload(defn);
  }

  public List<IStatement> overloadTheta(ErrorReport errors, List<IStatement> stmts, Dictionary cxt)
  {
    List<IStatement> result = new ArrayList<IStatement>();
    List<List<IStatement>> groups = ContractDependencies.dependencySort(stmts);

    Dictionary old = localCxt;
    localCxt = cxt.fork();

    for (List<IStatement> group : groups) {
      int mark = substitutionState();

      for (IStatement stmt : group) {

        if (group.size() > 1) {
          // phase I, declare other overloads.
          for (IStatement st : group)
            if (st instanceof VarEntry && st != stmt) {
              VarEntry defn = (VarEntry) st;
              IType varType = defn.getType();

              // Set up a substitution so that we can overload this variable
              if (TypeUtils.hasContractDependencies(varType) && !isOverloadedDefn(defn)) {
                OverloadedVariable var = (OverloadedVariable) defn.getVariable();

                defineSubstitution(var.getName(), var);
              }
            }
        }

        if (stmt instanceof VarEntry) {
          result.add(overload((VarEntry) stmt));
        } else
          result.add(stmt);
      }
      undoSubstitutionState(mark);
    }

    localCxt = old;
    return result;
  }

  public static IContentExpression resolve(Dictionary cxt, ErrorReport errors, IContentExpression exp)
  {
    OverLoader overloader = new OverLoader(cxt, cxt, errors);
    return overloader.transform(exp);
  }

  public static IContentAction resolve(Dictionary cxt, ErrorReport errors, IContentAction act)
  {
    OverLoader overloader = new OverLoader(cxt, cxt, errors);
    return overloader.transform(act);
  }

  private VarEntry overload(VarEntry defn)
  {
    IType varType = defn.getType();

    if (TypeUtils.hasContractDependencies(varType) && !isOverloadedDefn(defn)) {
      // We have a generic function that relies on the implementation of a
      // type contract
      // F(P1,..,Pn) is Exp
      //
      // We rewrite this to:
      // F(D) is let{ F'(P1,..,Pn) is Exp } in F'
      // where F is replaced by F' in Exp and F is replaced by F(D) in other expressions

      Location loc = defn.getLoc();
      Variable var = defn.getVariable();

      assert var instanceof OverloadedVariable;

      String vrName = var.getName();
      Dictionary trCxt = localCxt;
      localCxt = localCxt.fork();
      IContentExpression expression = defn.getValue();

      IType dictType = ((OverloadedVariable) var).getDictType();

      Variable innerVar = new Variable(loc, TypeUtils.getOverloadedType(dictType), vrName + "'");
      IContentExpression old = defineSubstitution(vrName, innerVar);

      IType[] reqTypes = TypeUtils.getOverloadRequirements(dictType);
      Variable reqVars[] = new Variable[reqTypes.length];

      int currDictState = dict.size();
      for (int ix = 0; ix < reqTypes.length; ix++) {
        IType reqType = reqTypes[ix];

        Variable dictVar = reqVars[ix] = new Variable(loc, reqType, reqType.typeLabel() + varNo++);
        localCxt.declareVar(dictVar.getName(), dictVar, AccessMode.readOnly, Visibility.priVate, true);
        dict.push(Pair.pair(reqType, (IContentExpression) dictVar));
      }

      IContentExpression resolvedExp = transform(expression);

      List<IStatement> inner = new ArrayList<IStatement>();

      inner.add(new VarEntry(loc, innerVar, resolvedExp, AccessMode.readOnly, Visibility.priVate));

      resolvedExp = new LetTerm(loc, innerVar, inner);

      Variable[] iFree = FreeVariables.freeFreeVars(reqVars, resolvedExp, trCxt);

      FunctionLiteral instFun = new FunctionLiteral(loc, vrName, dictType, reqVars, resolvedExp, iFree);

      localCxt = trCxt;

      // This is carefully done to avoid overloading a definition twice.
      Visibility visibility = defn.getVisibility();
      VarEntry resolved = new VarEntry(loc, Variable.create(loc, varType, vrName), instFun, AccessMode.readOnly,
          visibility);
      cxt.declareVar(vrName, Variable.create(loc, dictType, vrName), AccessMode.readOnly, visibility, true);

      defineSubstitution(vrName, old); // undo substitution
      dict.setSize(currDictState);

      return resolved;
    } else
      return (VarEntry) transform(defn);
  }

  private IContentExpression resolveOverloaded(OverloadedVariable var)
  {
    Location loc = var.getLoc();
    String varName = var.getName();

    IType overType = var.getDictType();

    IType reqs[] = TypeUtils.getOverloadRequirements(overType);
    IContentExpression args[] = new IContentExpression[reqs.length];

    for (int ix = 0; ix < args.length; ix++) {
      IType reqType = reqs[ix];

      assert reqType instanceof TypeExp;

      args[ix] = resolve(loc, reqType);

      if (args[ix] == null)
        return var; // not ready to overload, signal for overloading later
    }

    return new Resolved(loc, TypeUtils.getOverloadedType(overType), overType, new Variable(loc, overType, varName),
        args);
  }

  private static boolean isOverloadedDefn(VarEntry varEntry)
  {
    return TypeUtils.hasContractDependencies(varEntry.getType())
        && TypeUtils.isOverloadedType(varEntry.getValue().getType());
  }

  public static IType computeDictionaryType(IType conType, Location loc, AccessMode access)
  {
    List<TypeVar> uniVars = new ArrayList<TypeVar>();
    IType unwrapped = TypeUtils.unwrap(conType, uniVars);
    List<IType> reqVars = new ArrayList<IType>();

    findTypeContracts(reqVars, uniVars);

    Map<String, TypeVar> boundMap = new HashMap<String, TypeVar>();

    for (TypeVar tVar : uniVars)
      boundMap.put(tVar.typeLabel(), new TypeVar(tVar.getVarName(), tVar.getOriginalName(), access));

    List<IType> requires = new ArrayList<IType>();

    for (TypeVar tVar : uniVars) {
      TypeVar repl = (TypeVar) boundMap.get(tVar.typeLabel());

      for (ITypeConstraint con : (TypeVar) tVar) {
        if (con instanceof FieldConstraint) {
          FieldConstraint recCon = (FieldConstraint) con;
          TypeUtils.setFieldConstraint(repl, loc, recCon.getField(), Refresher.rewrite(recCon.getType(), boundMap));
        } else if (con instanceof FieldTypeConstraint) {
          FieldTypeConstraint recCon = (FieldTypeConstraint) con;
          TypeUtils.setTypeConstraint(repl, recCon.getName(), Refresher.rewrite(recCon.getType(), boundMap));
        }
      }
    }

    for (IType req : reqVars)
      requires.add(Refresher.rewrite(req, boundMap));

    return UniversalType.univ(boundMap.values(), TypeUtils.overloadedType(requires, Refresher.rewrite(unwrapped,
        boundMap)));
  }

  public static IType computeConstrainedType(IType type)
  {
    if (TypeUtils.isOverloadedType(type)) {
      Map<String, TypeVar> tVars = new HashMap<String, TypeVar>();
      IType tp = TypeUtils.deRef(type);

      while (tp instanceof UniversalType) {
        UniversalType univ = (UniversalType) tp;
        TypeVar bound = univ.getBoundVar();
        String name = bound.getVarName();
        tVars.put(name, new TypeVar(name, bound.getOriginalName(), AccessMode.readOnly));
        tp = univ.getBoundType();
      }

      IType rTp = Refresher.refresh(tp, tVars);

      IType[] requirements = TypeUtils.getOverloadRequirements(rTp);
      for (int ix = 0; ix < requirements.length; ix++) {
        assert requirements[ix] instanceof TypeExp;
        TypeExp contract = (TypeExp) requirements[ix];

        IType argTypes[] = contract.getTypeArgs();
        for (IType aType : argTypes) {
          aType = TypeUtils.deRef(aType);
          if (TypeUtils.isTypeVar(aType))
            ((TypeVar) aType).setConstraint(new ContractConstraint(contract));
        }
      }
      rTp = TypeUtils.getOverloadedType(rTp);

      return UniversalType.univ(tVars.values(), rTp);
    } else
      return type;
  }

  private static void findTypeContracts(List<IType> reqVars, Collection<TypeVar> typeVars)
  {
    for (TypeVar tv : typeVars) {
      reqLoop: for (ITypeConstraint con : tv) {
        if (con instanceof ContractConstraint) {
          TypeExp req = ((ContractConstraint) con).getContract();
          for (IType conType : reqVars) {
            if (conType.equals(req))
              continue reqLoop;
          }

          reqVars.add(req);
        }
      }
    }
  }
}
